Step of Proof: p-fun-exp-add-sq 11,40
Inference at * 2 2 1 2 1 1 1 
Iof proof for Lemma p-fun-exp-add-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
9. (n = 0)
10. (n+m = 0)
11. (n = 0)
12. (m = 0)
13. can-apply(f^m - 1;x)
14. x1 : A
15. do-apply(f^m - 1;x) = x1
  can-apply(f;x1) 
latex
 by (NthHypSq 8) 
CollapseTHEN ((EqCD) 
CollapseTHEN ((Auto) 
CollapseTHEN ((Unfold `can-apply
C` ( 0)) 
CollapseTHEN ((EqCD) 
CollapseTHEN (Auto))))) 
latex

C1: .....subterm..... T:t1:n

C1:   f(x1) = f^m(x)
C.

Definitionss ~ t, SQType(T), {T}, , can-apply(f;x), isl(x), f(a), Type, T, True, t  T, x:A. B(x), , {x:A| B(x)} , , A  B, A, False, P  Q, s = t, left + right, Top, n+m
Lemmasbool sq, isl wf

origin